Preliminary User's Manual                              March 26, 1973


V. SEARCHING AND PATTERN MATCHING.

The pattern matching  facilities for interactive theorem  proving are

the most difficult feature  to describe well. The tools  presented to

the user should be general enough to significantly aid in  the search

for a proof.  At the  same time the pattern matching  commands should

be  concise  and  somewhat readable.   Clearly,  pattern  matching is

present  throughout the  theorem prover;  the choice  strategies, the

rules of inference,  and the editing  strategies are all  examples of

very sophisticated pattern  matching. Thus pattern matching  is  very

important  part  of  the  theorem  proving  process.  Indeed  we  are

currently  exploring a  general theroem  proving language  which will

exploit pattern  matching in  all aspects of  proof search  -- rules,

strategies,  and  heuristics.   Currently,  a  very   simple  pattern

matching facility is available.

Pattern    matching    is   invoked    by    the    FIND   operation.

FIND[<id>,<pattern>]  expects  <id>  to  be the  name  of  a  list of

clauses, and <pattern> should  be a Boolean combination  of primitive

patterns. These primitive patterns are described in the next section,

but basically allow description of syntactic parts of clauses.

Since   many  of   the  applications   of  FIND   are  of   the  form

FIND[CLAUSES,<pattern>], the abbreviation, FINDC[<pattern>]  has been

added for this case.

Here's an example of FIND and FINDC.
SET XX FINDC[OCR[0]];   |OCR is a reserved word. The pattern says
                        |find all clauses in the set CLAUSES which 
                        |have occurrences of the symbol 0.
Preliminary User's Manual                              March 26, 1973


                        |In this problem 0 is a function letter.
*
DI XX;                  |Display the clauses.

1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*

SET YY FIND[XX,OCR[≤]]; |Find all clauses in XX which have occurrence
                        |of the symbol '≤', and assign those clauses 
                        |to YY.
*
DI YY;                  |Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*

*
SET ZZ FIND[YY,OCR[/]∧OCR[=]];|Boolean combinations are allowed.
*
SET ZZ FIND[YY,LENGTH=1];|This command will locate all units in the 
                        |set, YY.
Preliminary User's Manual                              March 26, 1973


VI. PRIMITIVE PATTERN LANGUAGE.

The currently available primitives allow description of   ancestry of

a  clause,  the  length(number  of  literals)  and  depth(of function

nesting) of  clauses,besides a very  simple matching  algorithm.  The

matcher   looks for  matches on  literals ,terms,  predicate letters,

negations of predicate letters, or fuctions symbols.

PRIMITIVES:

1) primitive for ancestry:  TREE[x]

"x"  designates  a  clause.   TREE[x]  will  match  any  clause whose

derivation  tree  contains  x.   N.B.   the  clause  ,x,   itself  is

considered to be derived from x.

Examples:

For example, if G1 is the name of an initial statement then :

SET YY FIND[XX,TREE[G1]]; will assign to YY all of the clauses  in XX

which were derived using G1.

2) primitive for length:   LENGTH

LENGTH gives  the number  of literals in  the clauses  currenly being

examined.  LENGTH may be tested using one of the available operators.

Examples:

LENGTH = 1 is true of the current clauses is a unit.

3) primitive for depth:    DEPTH

This primitive gives the depth of function nesting in the clause.

Example:
Preliminary User's Manual                              March 26, 1973


DEPTH > 4 is  true is the depth of  nesting of the current  clause is

greater than 4.

Primitive operators:

Currently the only operators availabel are  =,>,and <.  These operato
are only to be used in comparing length and depth.


MATCHING:

4) primitive for matching: OCR

OCR  is the  implementation  of a  simple matcher  which  expects its

arguments to be a literal, term,  predicate letter, or negation  of a

predicate letter.  OCR matches  any clause which contains  a matching

construct.

Variables  may appear  in  the pattern,  in  which case   a  test for

subsumption determines when a match is to be successful.

Examples:

In the following, assume P, and = are predicate letters;  assume x,y,

and z  are variables;  and assume a,b,c,d  and f  and g  are function

symbols.

OCR[P] matches P(x) ,P(a)⊃a=b, and ¬P(b).

OCR[¬P] matches P(a)⊃a=b and ¬P(b). Note P(a)⊃a=b matches  here since

the implication really is ¬P(a) ∨ a=b;

OCR[¬=]∧¬OCR[d] would match ¬f(a,b)=c but would not match ¬f(a,b)=d.

OCR[P(x)] matches P(x),¬P(g(x)) and ¬P(a).

OCR[¬P(g(x))] matches ¬P(g(a)) but not P(g(a)) or ¬P(f(g(a),x));
Preliminary User's Manual                              March 26, 1973


OCR[f(g(x),x)] matches clauses containing say, f(g(a),a) but does not

match f(g(a)b).